Nuprl Lemma : l_index_wf
0,22
postcript
pdf
T
:Type,
dT
:EqDecider(
T
),
L
:
T
List,
x
:
T
. (
x
L
)
index(
L
;
x
)
||
L
||
latex
Definitions
P
Q
,
P
Q
,
A
&
B
,
i
j
<
k
,
P
&
Q
,
(
x
l
)
,
EqDecider(
T
)
,
index(
L
;
x
)
,
,
A
B
,
A
,
False
,
i
j
,
||
as
||
,
eqof(
d
)
,
l
[
i
]
,
P
Q
,
x
:
A
.
B
(
x
)
,
t
T
,
x
:
A
.
B
(
x
)
,
b
,
{
i
..
j
}
Lemmas
int
seg
wf
,
select
wf
,
eqof
wf
,
length
wf1
,
non
neg
length
,
mu-bound
,
deq
wf
,
l
member
wf
,
le
wf
,
assert
wf
,
deq
property
origin
T:Type, dT:EqDecider(T), L:T List, x:T. (x 
L) 
index(L;x) 
||L|| T:Type, dT:EqDecider(T), L:T List, x:T. (x L) index(L;x) ||L|| 
Q Q
j < k l)B
A
j Qx:A. B(x) T
x:A. B(x)
b
}